YES 1.695
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ BR
mainModule Main
| (((==) :: (Eq a, Eq b) => Either a b -> Either a b -> Bool) :: (Eq b, Eq a) => Either a b -> Either a b -> Bool) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| (((==) :: (Eq b, Eq a) => Either b a -> Either b a -> Bool) :: (Eq a, Eq b) => Either b a -> Either b a -> Bool) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| ((==) :: (Eq a, Eq b) => Either a b -> Either a b -> Bool) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(xv2200), Succ(xv400000)) → new_primPlusNat(xv2200, xv400000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(xv2200), Succ(xv400000)) → new_primPlusNat(xv2200, xv400000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(xv30000), Succ(xv40000)) → new_primMulNat(xv30000, Succ(xv40000))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(xv30000), Succ(xv40000)) → new_primMulNat(xv30000, Succ(xv40000))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(xv3000), Succ(xv4000)) → new_primEqNat(xv3000, xv4000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(xv3000), Succ(xv4000)) → new_primEqNat(xv3000, xv4000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_esEs3(Just(xv300), Just(xv400), app(app(ty_@2, bbf), bbg)) → new_esEs1(xv300, xv400, bbf, bbg)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(ty_[], fd)), bag) → new_esEs0(xv300, xv400, fd)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(ty_[], baa)), hh), bag) → new_esEs0(xv300, xv400, baa)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(app(ty_@3, dg), dh), ea)), bb), cg), bag) → new_esEs(xv300, xv400, dg, dh, ea)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], eh), bag) → new_esEs0(xv301, xv401, eh)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(app(app(ty_@3, fa), fb), fc)), bag) → new_esEs(xv300, xv400, fa, fb, fc)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, bb, app(ty_[], bf)) → new_esEs0(xv302, xv402, bf)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, gc), app(app(ty_@2, gh), ha)), bag) → new_esEs1(xv301, xv401, gh, ha)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(ty_[], baa), hh) → new_esEs0(xv300, xv400, baa)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, gc), app(ty_Maybe, hd)), bag) → new_esEs3(xv301, xv401, hd)
new_esEs2(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(ty_[], bbe)), bag) → new_esEs0(xv300, xv400, bbe)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(app(app(ty_@3, fa), fb), fc)) → new_esEs(xv300, xv400, fa, fb, fc)
new_esEs2(Left(xv30), Left(xv40), app(app(ty_Either, bah), bba), bag) → new_esEs2(xv30, xv40, bah, bba)
new_esEs3(Just(xv300), Just(xv400), app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs(xv300, xv400, bbb, bbc, bbd)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), gc, app(ty_[], gg)) → new_esEs0(xv301, xv401, gg)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, gc), app(app(app(ty_@3, gd), ge), gf)), bag) → new_esEs(xv301, xv401, gd, ge, gf)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, app(app(ty_Either, dd), de), cg) → new_esEs2(xv301, xv401, dd, de)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(app(app(ty_@3, he), hf), hg)), hh), bag) → new_esEs(xv300, xv400, he, hf, hg)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), bb), app(app(app(ty_@3, bc), bd), be)), bag) → new_esEs(xv302, xv402, bc, bd, be)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(ty_Maybe, gb)), bag) → new_esEs3(xv300, xv400, gb)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(ty_Either, ee), ef)), bb), cg), bag) → new_esEs2(xv300, xv400, ee, ef)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), gc, app(app(ty_@2, gh), ha)) → new_esEs1(xv301, xv401, gh, ha)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), app(ty_[], da)), cg), bag) → new_esEs0(xv301, xv401, da)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(app(ty_@2, ff), fg)) → new_esEs1(xv300, xv400, ff, fg)
new_esEs2(Right(xv30), Right(xv40), bcc, app(app(ty_Either, bdb), bdc)) → new_esEs2(xv30, xv40, bdb, bdc)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_Either, ee), ef), bb, cg) → new_esEs2(xv300, xv400, ee, ef)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), app(app(app(ty_@3, cd), ce), cf)), cg), bag) → new_esEs(xv301, xv401, cd, ce, cf)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), app(ty_Maybe, df)), cg), bag) → new_esEs3(xv301, xv401, df)
new_esEs2(Right(xv30), Right(xv40), bcc, app(ty_Maybe, bdd)) → new_esEs3(xv30, xv40, bdd)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), gc, app(app(ty_Either, hb), hc)) → new_esEs2(xv301, xv401, hb, hc)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), app(app(ty_Either, dd), de)), cg), bag) → new_esEs2(xv301, xv401, dd, de)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(ty_@2, ec), ed)), bb), cg), bag) → new_esEs1(xv300, xv400, ec, ed)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), bb), app(ty_Maybe, cc)), bag) → new_esEs3(xv302, xv402, cc)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_@2, ec), ed), bb, cg) → new_esEs1(xv300, xv400, ec, ed)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(ty_Maybe, eg)), bb), cg), bag) → new_esEs3(xv300, xv400, eg)
new_esEs2(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(ty_Maybe, bcb)), bag) → new_esEs3(xv300, xv400, bcb)
new_esEs2(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(app(ty_Either, bbh), bca)), bag) → new_esEs2(xv300, xv400, bbh, bca)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(app(ty_@2, bab), bac)), hh), bag) → new_esEs1(xv300, xv400, bab, bac)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), app(app(ty_@2, db), dc)), cg), bag) → new_esEs1(xv301, xv401, db, dc)
new_esEs0(:(xv300, xv301), :(xv400, xv401), eh) → new_esEs0(xv301, xv401, eh)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), gc, app(ty_Maybe, hd)) → new_esEs3(xv301, xv401, hd)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_Maybe, eg), bb, cg) → new_esEs3(xv300, xv400, eg)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_Either, bad), bae), hh) → new_esEs2(xv300, xv400, bad, bae)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(ty_Maybe, gb)) → new_esEs3(xv300, xv400, gb)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, app(ty_[], da), cg) → new_esEs0(xv301, xv401, da)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, app(app(ty_@2, db), dc), cg) → new_esEs1(xv301, xv401, db, dc)
new_esEs2(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(app(app(ty_@3, bbb), bbc), bbd)), bag) → new_esEs(xv300, xv400, bbb, bbc, bbd)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(app(ty_Either, bad), bae)), hh), bag) → new_esEs2(xv300, xv400, bad, bae)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(ty_Maybe, baf), hh) → new_esEs3(xv300, xv400, baf)
new_esEs2(Right(xv30), Right(xv40), bcc, app(app(ty_@2, bch), bda)) → new_esEs1(xv30, xv40, bch, bda)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(app(ty_@3, dg), dh), ea), bb, cg) → new_esEs(xv300, xv400, dg, dh, ea)
new_esEs3(Just(xv300), Just(xv400), app(ty_[], bbe)) → new_esEs0(xv300, xv400, bbe)
new_esEs3(Just(xv300), Just(xv400), app(app(ty_Either, bbh), bca)) → new_esEs2(xv300, xv400, bbh, bca)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, bb, app(app(ty_@2, bg), bh)) → new_esEs1(xv302, xv402, bg, bh)
new_esEs2(Right(xv30), Right(xv40), bcc, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs(xv30, xv40, bcd, bce, bcf)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), bb), app(ty_[], bf)), bag) → new_esEs0(xv302, xv402, bf)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, bb, app(app(ty_Either, ca), cb)) → new_esEs2(xv302, xv402, ca, cb)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(app(ty_Either, fh), ga)), bag) → new_esEs2(xv300, xv400, fh, ga)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, app(app(app(ty_@3, cd), ce), cf), cg) → new_esEs(xv301, xv401, cd, ce, cf)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(app(ty_Either, fh), ga)) → new_esEs2(xv300, xv400, fh, ga)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, app(ty_Maybe, df), cg) → new_esEs3(xv301, xv401, df)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_@2, bab), bac), hh) → new_esEs1(xv300, xv400, bab, bac)
new_esEs2(Right(xv30), Right(xv40), bcc, app(ty_[], bcg)) → new_esEs0(xv30, xv40, bcg)
new_esEs3(Just(xv300), Just(xv400), app(ty_Maybe, bcb)) → new_esEs3(xv300, xv400, bcb)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, gc), app(ty_[], gg)), bag) → new_esEs0(xv301, xv401, gg)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), bb), app(app(ty_Either, ca), cb)), bag) → new_esEs2(xv302, xv402, ca, cb)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, bb, app(ty_Maybe, cc)) → new_esEs3(xv302, xv402, cc)
new_esEs2(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(app(ty_@2, ff), fg)), bag) → new_esEs1(xv300, xv400, ff, fg)
new_esEs2(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(app(ty_@2, bbf), bbg)), bag) → new_esEs1(xv300, xv400, bbf, bbg)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_[], eb), bb, cg) → new_esEs0(xv300, xv400, eb)
new_esEs0(:(xv300, xv301), :(xv400, xv401), app(ty_[], fd)) → new_esEs0(xv300, xv400, fd)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), gc, app(app(app(ty_@3, gd), ge), gf)) → new_esEs(xv301, xv401, gd, ge, gf)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), bb), app(app(ty_@2, bg), bh)), bag) → new_esEs1(xv302, xv402, bg, bh)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, gc), app(app(ty_Either, hb), hc)), bag) → new_esEs2(xv301, xv401, hb, hc)
new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(ty_Maybe, baf)), hh), bag) → new_esEs3(xv300, xv400, baf)
new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(ty_[], eb)), bb), cg), bag) → new_esEs0(xv300, xv400, eb)
new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(app(app(ty_@3, he), hf), hg), hh) → new_esEs(xv300, xv400, he, hf, hg)
new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, bb, app(app(app(ty_@3, bc), bd), be)) → new_esEs(xv302, xv402, bc, bd, be)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs0(:(xv300, xv301), :(xv400, xv401), app(ty_Maybe, gb)) → new_esEs3(xv300, xv400, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(xv300, xv301), :(xv400, xv401), app(app(ty_Either, fh), ga)) → new_esEs2(xv300, xv400, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(xv300, xv301), :(xv400, xv401), app(app(app(ty_@3, fa), fb), fc)) → new_esEs(xv300, xv400, fa, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(xv300, xv301), :(xv400, xv401), app(app(ty_@2, ff), fg)) → new_esEs1(xv300, xv400, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(xv300), Just(xv400), app(ty_Maybe, bcb)) → new_esEs3(xv300, xv400, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(Just(xv300), Just(xv400), app(app(ty_Either, bbh), bca)) → new_esEs2(xv300, xv400, bbh, bca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(xv300), Just(xv400), app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs(xv300, xv400, bbb, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(Just(xv300), Just(xv400), app(app(ty_@2, bbf), bbg)) → new_esEs1(xv300, xv400, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(Just(xv300), Just(xv400), app(ty_[], bbe)) → new_esEs0(xv300, xv400, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), gc, app(ty_Maybe, hd)) → new_esEs3(xv301, xv401, hd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(ty_Maybe, baf), hh) → new_esEs3(xv300, xv400, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), gc, app(app(ty_Either, hb), hc)) → new_esEs2(xv301, xv401, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_Either, bad), bae), hh) → new_esEs2(xv300, xv400, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), gc, app(app(app(ty_@3, gd), ge), gf)) → new_esEs(xv301, xv401, gd, ge, gf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(app(app(ty_@3, he), hf), hg), hh) → new_esEs(xv300, xv400, he, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), gc, app(app(ty_@2, gh), ha)) → new_esEs1(xv301, xv401, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_@2, bab), bac), hh) → new_esEs1(xv300, xv400, bab, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), app(ty_[], baa), hh) → new_esEs0(xv300, xv400, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@2(xv300, xv301), @2(xv400, xv401), gc, app(ty_[], gg)) → new_esEs0(xv301, xv401, gg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_Maybe, eg), bb, cg) → new_esEs3(xv300, xv400, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, app(ty_Maybe, df), cg) → new_esEs3(xv301, xv401, df)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, bb, app(ty_Maybe, cc)) → new_esEs3(xv302, xv402, cc)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, gc), app(ty_Maybe, hd)), bag) → new_esEs3(xv301, xv401, hd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(ty_Maybe, gb)), bag) → new_esEs3(xv300, xv400, gb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), app(ty_Maybe, df)), cg), bag) → new_esEs3(xv301, xv401, df)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xv30), Right(xv40), bcc, app(ty_Maybe, bdd)) → new_esEs3(xv30, xv40, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), bb), app(ty_Maybe, cc)), bag) → new_esEs3(xv302, xv402, cc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(ty_Maybe, eg)), bb), cg), bag) → new_esEs3(xv300, xv400, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(ty_Maybe, bcb)), bag) → new_esEs3(xv300, xv400, bcb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(ty_Maybe, baf)), hh), bag) → new_esEs3(xv300, xv400, baf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(xv300, xv301), :(xv400, xv401), eh) → new_esEs0(xv301, xv401, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs0(:(xv300, xv301), :(xv400, xv401), app(ty_[], fd)) → new_esEs0(xv300, xv400, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, app(app(ty_Either, dd), de), cg) → new_esEs2(xv301, xv401, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_Either, ee), ef), bb, cg) → new_esEs2(xv300, xv400, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, bb, app(app(ty_Either, ca), cb)) → new_esEs2(xv302, xv402, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs2(Left(xv30), Left(xv40), app(app(ty_Either, bah), bba), bag) → new_esEs2(xv30, xv40, bah, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(ty_Either, ee), ef)), bb), cg), bag) → new_esEs2(xv300, xv400, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xv30), Right(xv40), bcc, app(app(ty_Either, bdb), bdc)) → new_esEs2(xv30, xv40, bdb, bdc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), app(app(ty_Either, dd), de)), cg), bag) → new_esEs2(xv301, xv401, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(app(ty_Either, bbh), bca)), bag) → new_esEs2(xv300, xv400, bbh, bca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(app(ty_Either, bad), bae)), hh), bag) → new_esEs2(xv300, xv400, bad, bae)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(app(ty_Either, fh), ga)), bag) → new_esEs2(xv300, xv400, fh, ga)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), bb), app(app(ty_Either, ca), cb)), bag) → new_esEs2(xv302, xv402, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, gc), app(app(ty_Either, hb), hc)), bag) → new_esEs2(xv301, xv401, hb, hc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(app(ty_@3, dg), dh), ea), bb, cg) → new_esEs(xv300, xv400, dg, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, app(app(app(ty_@3, cd), ce), cf), cg) → new_esEs(xv301, xv401, cd, ce, cf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, bb, app(app(app(ty_@3, bc), bd), be)) → new_esEs(xv302, xv402, bc, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_@2, ec), ed), bb, cg) → new_esEs1(xv300, xv400, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, app(app(ty_@2, db), dc), cg) → new_esEs1(xv301, xv401, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, bb, app(app(ty_@2, bg), bh)) → new_esEs1(xv302, xv402, bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, bb, app(ty_[], bf)) → new_esEs0(xv302, xv402, bf)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), ba, app(ty_[], da), cg) → new_esEs0(xv301, xv401, da)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_[], eb), bb, cg) → new_esEs0(xv300, xv400, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(app(ty_@3, dg), dh), ea)), bb), cg), bag) → new_esEs(xv300, xv400, dg, dh, ea)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(app(app(ty_@3, fa), fb), fc)), bag) → new_esEs(xv300, xv400, fa, fb, fc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, gc), app(app(app(ty_@3, gd), ge), gf)), bag) → new_esEs(xv301, xv401, gd, ge, gf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(app(app(ty_@3, he), hf), hg)), hh), bag) → new_esEs(xv300, xv400, he, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), bb), app(app(app(ty_@3, bc), bd), be)), bag) → new_esEs(xv302, xv402, bc, bd, be)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), app(app(app(ty_@3, cd), ce), cf)), cg), bag) → new_esEs(xv301, xv401, cd, ce, cf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(app(app(ty_@3, bbb), bbc), bbd)), bag) → new_esEs(xv300, xv400, bbb, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Right(xv30), Right(xv40), bcc, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs(xv30, xv40, bcd, bce, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, gc), app(app(ty_@2, gh), ha)), bag) → new_esEs1(xv301, xv401, gh, ha)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(app(ty_@2, ec), ed)), bb), cg), bag) → new_esEs1(xv300, xv400, ec, ed)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(app(ty_@2, bab), bac)), hh), bag) → new_esEs1(xv300, xv400, bab, bac)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), app(app(ty_@2, db), dc)), cg), bag) → new_esEs1(xv301, xv401, db, dc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Right(xv30), Right(xv40), bcc, app(app(ty_@2, bch), bda)) → new_esEs1(xv30, xv40, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs2(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(app(ty_@2, bbf), bbg)), bag) → new_esEs1(xv300, xv400, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(app(ty_@2, ff), fg)), bag) → new_esEs1(xv300, xv400, ff, fg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), bb), app(app(ty_@2, bg), bh)), bag) → new_esEs1(xv302, xv402, bg, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], app(ty_[], fd)), bag) → new_esEs0(xv300, xv400, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, app(ty_[], baa)), hh), bag) → new_esEs0(xv300, xv400, baa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(:(xv300, xv301)), Left(:(xv400, xv401)), app(ty_[], eh), bag) → new_esEs0(xv301, xv401, eh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(Just(xv300)), Left(Just(xv400)), app(ty_Maybe, app(ty_[], bbe)), bag) → new_esEs0(xv300, xv400, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), app(ty_[], da)), cg), bag) → new_esEs0(xv301, xv401, da)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, ba), bb), app(ty_[], bf)), bag) → new_esEs0(xv302, xv402, bf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Right(xv30), Right(xv40), bcc, app(ty_[], bcg)) → new_esEs0(xv30, xv40, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs2(Left(@2(xv300, xv301)), Left(@2(xv400, xv401)), app(app(ty_@2, gc), app(ty_[], gg)), bag) → new_esEs0(xv301, xv401, gg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Left(@3(xv300, xv301, xv302)), Left(@3(xv400, xv401, xv402)), app(app(app(ty_@3, app(ty_[], eb)), bb), cg), bag) → new_esEs0(xv300, xv400, eb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3